STM: poset sig inc

ABS: DSet

STM: dset wf

STM: dset properties

STM: assert of dset eq

STM: decidable dset eq

STM: dset eq refl

ABS: mk_dset(T, eq)

STM: mk dset wf

ABS: a  b

STM: set leq wf

STM: decidable set leq

STM: assert of set leq

ABS: a < b

STM: set blt wf

STM: comb for set blt wf

ABS: a <p b

STM: set lt wf

STM: set lt is sp of leq

STM: set lt is sp of leq a

STM: decidable set lt

STM: assert of set lt

ABS: QOSet

STM: qoset wf

STM: qoset properties

STM: qoset refl

STM: set leq weakening eq

STM: qoset trans

STM: set leq transitivity

STM: set leq trans

STM: qoset lt trans

STM: qoset lt irrefl

STM: set lt irreflexivity

STM: set leq weakening lt

STM: set lt transitivity 1

STM: set lt transitivity 2

STM: set blt functionality wrt set lt r

ABS: POSet{i}

STM: poset wf

STM: poset properties

STM: poset anti sym

STM: set leq antisymmetry

STM: set leq iff lt or eq

ABS: LOSet

STM: loset wf

STM: loset properties

ABS: mk_oset(T;eq;leq)

STM: mk oset wf

STM: loset connex

STM: loset trichot

STM: set leq complement

STM: set lt complement

ABS: a = b

STM: eq pair wf

STM: assert of eq pair

ABS: s  t

STM: set prod wf

ABS: {x:s| Q(x) }

STM: eqfun p subtyping

STM: dset set wf

ABS: int_loset()

STM: int loset wf

ABS: atom_dset()

STM: atom dset wf

Up

Algebra